$\forall$$A$:Type, $L$, $L_{1}$, $L_{2}$:$A$ List, $f_{1}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$), $f_{2}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$).
\\[0ex]interleaving\_occurence($A$;$L_{1}$;$L_{2}$;$L$;$f_{1}$;$f_{2}$)
\\[0ex]$\Rightarrow$ ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. ($\exists$$k$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$. $j$ $=$ $f_{1}$($k$) $\in$ $\mathbb{Z}$) $\vee$ ($\exists$$k$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$. $j$ $=$ $f_{2}$($k$) $\in$ $\mathbb{Z}$))